!bench

Benchmark results for 8418eab against 9268b22 are in. No significant results found. @yuanyi-350

• 🟥 build//instructions: +4.2G (+0.00%)

Small changes (2🟥)

• 🟥 build/module/Mathlib.Data.Char//instructions: +124.6M (+5.27%)
• 🟥 build/module/Mathlib.MeasureTheory.MeasurableSpace.Card//instructions: +424.2M (+3.53%)

PR summary 9268b22206

Import changes for modified files

No significant changes to the import graph

Declarations diff

No declarations were harmed in the making of this PR! 🐙

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

I ran a profiler comparison for the changed declarations in this PR.

Results (seconds):

• IsPrimitiveRoot.autToPow_injective: 0.117810 -> 0.032246 (-72.63%)

Overall:

• IsPrimitiveRoot.autToPow_injective elaborates substantially faster after the refactor.

🚀 Pull request has been placed on the maintainer queue by MichaelStollBayreuth.

Are you abusing defeq here?

@riccardobrasca , My bad, I definitely used the defeq between AlgEquiv and toAlgHom before! This new update should be standard, though. I'm really curious, how do you usually catch this sort of defeq abuse? Is it just intuition? I was wondering if we could try automating the defeq abuse detection process to help out the community better.

1. Mathlib/NumberTheory/Cyclotomic/Gal.lean:59

Code: apply AlgEquiv.coe_algHom_injective

Actual state transition in the proof:
Before:

⊢ f = g

After:

⊢ (f : L →ₐ[K] L) = (g : L →ₐ[K] L)

Designed state transition from the theorem type:

AlgHomClass.toAlgHom.Injective

2. Mathlib/NumberTheory/Cyclotomic/Gal.lean:60

Code: apply (hμ.powerBasis K).algHom_ext

Actual state transition in the proof:
Before:

⊢ (f : L →ₐ[K] L) = (g : L →ₐ[K] L)

After:

⊢ (f : L →ₐ[K] L) ((hμ.powerBasis K).gen : L) =
     (g : L →ₐ[K] L) ((hμ.powerBasis K).gen : L)

Designed state transition from the theorem type:

((f : L →ₐ[K] L) ((hμ.powerBasis K).gen : L) =
(g : L →ₐ[K] L) ((hμ.powerBasis K).gen : L)) →
(f : L →ₐ[K] L) = (g : L →ₐ[K] L)

Are these answers written by an LLM?

The initial commit was LLM-generated, but I made the subsequent changes myself based on your feedback. Currently, LLMs just don't understand defeq abuse.

The state analysis below is the experimental workflow I typed out manually. If I were to automate this part and provide this kind of information for every PR, do you think it would significantly reduce occurrences of defeq abuse?

There are already various discussion on Zulip about this, it's not completely clear how much of defeq abuse we want, so we currently decide case by case. Anyway this PR lgtm, thanks!

bors merge

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-CI job
• ci (staging) / Lint style
• ci (staging) / Post-Build Step
• ci (staging) / Build